Inference at * 
Iof proof for Lemma integer sqrt:


  n:. r:. (((r * r)  n) & (n < ((r+1) * (r+1)))) 

latex

 by D 0 THENA Auto 

latex

 1: 

 1: 1. n : 
 1:   r:. (((r * r)  n) & (n < ((r+1) * (r+1))))
 .

Definitions	x:A. B(x), x:A. B(x), P & Q, x:A  B(x), a < b, A  B, x:AB(x), , t  T, s = t
Lemmas	le wf, nat wf